#![feature(rustc_private)]
#[macro_use]
mod common;
use common::*;

test_verify_one_file! {
    #[test] basics verus_code! {
        use vstd::prelude::*;
        use vstd::raw_ptr::*;

        fn test_mut_const_casts(x: *mut u8) {
            let y = x as *const u8;
            let z = y as *const u8;
            assert(z == x);
            assert(z == y);
        }

        fn test_addr_doesnt_imply_eq(x: *mut u8, y: *mut u8) {
            assume(x@.addr == y@.addr);
            assert(x == y); // FAILS
        }

        fn test_view_does_imply_eq(x: *mut u8, y: *mut u8) {
            assume(x@ == y@);
            assert(x == y);
        }

        fn test_view_does_imply_eq_const(x: *const u8, y: *const u8) {
            assume(x@ == y@);
            assert(x == y);
        }

        fn test_null() {
            let x: *const u8 = core::ptr::null();
            let y: *mut u8 = core::ptr::null_mut();
            assert(x == y);
            assert(x@.addr == 0);
        }

        fn test_manipulating(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            let tracked mut pt = pt;

            assume(x == pt.ptr());
            assume(pt.is_uninit());

            ptr_mut_write(x, Tracked(&mut pt), 20);

            assert(x == pt.ptr());
            assert(pt.is_init());
            assert(pt.value() == 20);

            let val = ptr_ref(x, Tracked(&pt));

            assert(val == 20);

            let val = ptr_mut_read(x, Tracked(&mut pt));

            assert(val == 20);
            assert(x == pt.ptr());
            assert(pt.is_uninit());
        }

        fn test_manipulating2(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            let tracked mut pt = pt;

            assume(x == pt.ptr());
            assume(pt.is_uninit());

            ptr_mut_write(x, Tracked(&mut pt), 20);

            assert(x == pt.ptr());
            assert(pt.is_init());
            assert(pt.value() == 20);

            let val = ptr_ref(x, Tracked(&pt));

            assert(val == 20);

            let val = ptr_mut_read(x, Tracked(&mut pt));

            assert(val == 20);
            assert(x == pt.ptr());
            assert(pt.is_uninit());

            assert(false); // FAILS
        }

        fn test_ptr_mut_write_different(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            let tracked mut pt = pt;
            assume(pt.is_uninit());
            ptr_mut_write(x, Tracked(&mut pt), 20); // FAILS
        }

        fn test_ptr_mut_read_different(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            let tracked mut pt = pt;
            assume(pt.is_init());
            let _ = ptr_mut_read(x, Tracked(&mut pt)); // FAILS
        }

        fn test_ptr_ref_different(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            assume(pt.is_init());
            let _ = ptr_ref(x, Tracked(&pt)); // FAILS
        }

        fn test_ptr_mut_read_uninit(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            let tracked mut pt = pt;
            assume(pt.ptr() == x);
            let _ = ptr_mut_read(x, Tracked(&mut pt)); // FAILS
        }

        fn test_ptr_ref_uninit(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            assume(pt.ptr() == x);
            let _ = ptr_ref(x, Tracked(&pt)); // FAILS
        }

        fn cast_test(x: *mut u8) {
            let y = x as *mut u16;
            assert(y@.addr == x@.addr);
            assert(y@.provenance == x@.provenance);
            assert(y@.metadata == ());
        }

        fn cast_test2(x: *mut [u8]) {
            let y = x as *mut u16;
            assert(y@.addr == x@.addr);
            assert(y@.provenance == x@.provenance);
            assert(y@.metadata == ());
        }

        fn cast_test3(x: *mut [u64; 16]) {
            let y = x as *mut [u64];
            assert(y@.addr == x@.addr);
            assert(y@.provenance == x@.provenance);
            assert(y@.metadata == 16);
        }

        proof fn cast_proof_test(x: *mut u8) {
            let y = x as *mut u16;
            assert(y@.addr == x@.addr);
            assert(y@.provenance == x@.provenance);
            assert(y@.metadata == ());
        }

        proof fn cast_proof_test2(x: *mut [u8]) {
            let y = x as *mut u16;
            assert(y@.addr == x@.addr);
            assert(y@.provenance == x@.provenance);
            assert(y@.metadata == ());
        }

        proof fn cast_proof_test3(x: *mut [u64; 16]) {
            let y = x as *mut [u64];
            assert(y@.addr == x@.addr);
            assert(y@.provenance == x@.provenance);
            assert(y@.metadata == 16);
        }

        fn test_strict_provenance(a: *mut u64) {
            let ad = a.addr();
            assert(ad == a@.addr);

            let b = a.with_addr(7);
            assert(b@.addr == 7);
            assert(b@.provenance == a@.provenance);
            assert(b@.metadata == a@.metadata);

            assert(a == b); // FAILS
        }

        fn test_strict_provenance_const(a: *const u64) {
            let ad = a.addr();
            assert(ad == a@.addr);

            let b = a.with_addr(7);
            assert(b@.addr == 7);
            assert(b@.provenance == a@.provenance);
            assert(b@.metadata == a@.metadata);
        }

        fn test_extensionality_sized<T>(a: *const T, b: *const T) {
            assume(a.addr() == b.addr() && a@.provenance == b@.provenance);
            assert(a == b);
        }

        fn test_extensionality_unsized<T: ?Sized>(a: *const T, b: *const T) {
            assume(a.addr() == b.addr() && a@.provenance == b@.provenance);
            assert(a == b); // FAILS
        }

    } => Err(err) => assert_fails(err, 9)
}

test_verify_one_file! {
    #[test] pointer_cast_to_ints verus_code! {
        use vstd::prelude::*;
        use vstd::raw_ptr::*;

        proof fn test<T>(x: *mut T) {
            assert(x@.addr == x as int);
            assert(x@.addr == x as nat);
            assert(x@.addr == x as usize);
            assert(x@.addr as u16 == x as u16);
        }

        proof fn test_fails<T>(x: *mut T) {
            assert(x@.addr == x as u16); // FAILS
        }

        proof fn test_fails2<T>(x: *mut T) {
            assert(x@.addr == x as isize); // FAILS
        }

        fn exec_test<T>(x: *mut T) {
            let x1 = x as usize;
            assert(x@.addr == x1);

            let x2 = x as u16;
            assert(x@.addr as u16 == x2);
        }

        fn exec_test_fails<T>(x: *mut T) {
            let x1 = x as u16;
            assert(x@.addr == x1); // FAILS
        }

        fn exec_test_fails2<T>(x: *mut T) {
            let x1 = x as isize;
            assert(x@.addr == x1); // FAILS
        }
    } => Err(err) => assert_fails(err, 4)
}

test_verify_one_file! {
    #[test] pointer_exec_eq_is_not_spec_eq verus_code! {
        use vstd::prelude::*;
        fn test_const_eq(x: *const u8, y: *const u8) {
            if x == y {
                assert(x == y); // FAILS
            }
        }

        fn test_mut_eq(x: *mut u8, y: *mut u8) {
            if x == y {
                assert(x == y); // FAILS
            }
        }
    } => Err(err) => assert_fails(err, 2)
}

test_verify_one_file! {
    #[test] points_to_move_error verus_code! {
        use vstd::prelude::*;
        use vstd::raw_ptr::*;

        fn test(Tracked(pt): Tracked<PointsTo<u8>>) {
        }

        fn test2(Tracked(pt): Tracked<PointsTo<u8>>) {
            test(Tracked(pt));
            test(Tracked(pt));
        }
    } => Err(err) => assert_rust_error_msg(err, "use of moved value: `pt`")
}

test_verify_one_file! {
    #[test] ptr_ref_lifetime_error verus_code! {
        use vstd::prelude::*;
        use vstd::raw_ptr::*;

        fn test(Tracked(pt): Tracked<PointsTo<u8>>) {
        }

        fn test2(x: *mut u8, Tracked(pt): Tracked<PointsTo<u8>>) {
            assume(pt.is_init());
            assume(pt.ptr() == x);
            let y = ptr_ref(x, Tracked(&pt));

            test(Tracked(pt));

            let z = *y;
        }
    } => Err(err) => assert_rust_error_msg(err, "cannot move out of `pt` because it is borrowed")
}

test_verify_one_file! {
    #[test] not_supported_int_to_ptr_cast verus_code! {
        fn test(x: usize) {
            let y = x as *mut u8;
        }
    } => Err(err) => assert_vir_error_msg(err, "Verus does not support this cast")
}

test_verify_one_file! {
    #[test] not_supported_deref_ptr verus_code! {
        pub fn run(x: *mut u8) {
            unsafe { let y = *x; }
        }
    } => Err(err) => assert_vir_error_msg(err, "The verifier does not yet support the following Rust feature: dereferencing a raw pointer")
}

test_verify_one_file! {
    #[test] allocate_in_bounds verus_code! {
        use vstd::raw_ptr::*;
        use vstd::layout::layout_for_type_is_valid;
        use vstd::prelude::Set;

        global layout u32 is size == 4, align == 4;

        fn f() {
            layout_for_type_is_valid::<u32>();

            let (block_ptr, Tracked(token), Tracked(dealloc)) = allocate(8, 4);

            let b1_ptr = block_ptr as *mut u32;
            let b2_ptr = block_ptr.with_addr(block_ptr.addr() + 4) as *mut u32;

            let tracked (token1, token2) = token.split(Set::new(|x: int| block_ptr.addr() <= x < block_ptr.addr() + 4));
            let tracked mut token1 = token1.into_typed::<u32>(b1_ptr as usize);
            let tracked mut token2 = token2.into_typed::<u32>(b2_ptr as usize);

            ptr_mut_write(b1_ptr, Tracked(&mut token1), 9);
            ptr_mut_write(b2_ptr, Tracked(&mut token2), 14);
        }
    } => Ok(())
}
